$\forall$${\it es}$:ES, ${\it ff}$:FIFO, ${\it f2f+}$:F2F+{-}decls.
\\[0ex]plus{-}ify\{i:l\}(${\it es}$;${\it ff}$;is\_req  ;is\_ack ;awaiting ;owes\_ack )
\\[0ex]$\Rightarrow$ ($\forall$${\it sndr}$, ${\it rcvr}$:${\it ff}$.C, $y$:E. [$y$: ${\it rcvr}$ $--$is\_ack $\rightarrow$ ${\it sndr}$] $\Rightarrow$ ($\exists$$z$:E. f2f+{-}pred($z$,$y$)))